Nuprl Definition : R-interface-compat 11,40
R-interface-compat(A; B)
== if Rsends?(B)
== then if Reffect?(A)
== then ifthen let k = Reffect-knd(A) in
== then ifthen let kif band(isrcv(k); eq_lnk(lnk(k); Rsends-l(B)))
== then ifthen let then subtype_rel(fpf-cap(Rsends-dt(B); id-deq; tag(k); void); Reffect-T(A))
== then ifthen let else True
== then ifthen let fi 
== then if Rsends?(A)
== then ifthen let k = Rsends-knd(A) in
== then ifthen let kif band(isrcv(k); eq_lnk(lnk(k); Rsends-l(B)))
== then ifthen let then subtype_rel(fpf-cap(Rsends-dt(B); id-deq; tag(k); void); Rsends-T(A))
== then ifthen let else True
== then ifthen let fi 
== then else True
== then fi 
== else True
== fi  
latex

DefinitionsTrue, Rsends-T(x1), void, tag(k), id-deq, Rsends-dt(x1), fpf-cap(f; eq; x; z), Rsends-l(x1), lnk(k), eq_lnk(a; b), isrcv(k), band(p; q), if b then t else f fi , Rsends-knd(x1), let x = a in b(x), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1)
FDL editor aliasesR-interface-compat

origin